

LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c450335 c450334)) v (p c450335 c450334))


> hypdisj
=============================
Step 3

? (p c450335 c450334)

1. (pp c450335 c450334)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c450335 c450334)

1. (~ (p c450335 c450334))
2. (pp c450335 c450334)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c455464 c455463)) v (pp c455464 c455463))


> hypdisj
=============================
Step 3

? (pp c455464 c455463)

1. (tpp c455464 c455463)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c455464 c455463)

1. (~ (pp c455464 c455463))
2. (tpp c455464 c455463)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c460649 c460648)) v (pp c460649 c460648))


> hypdisj
=============================
Step 3

? (pp c460649 c460648)

1. (ntpp c460649 c460648)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c460649 c460648)

1. (~ (pp c460649 c460648))
2. (ntpp c460649 c460648)

> hyp


LEMMA

Parthood lifts connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c465892 c465891)) v (~ (c c465890 c465892))) v (c c465890 c465891))


> hypdisj
=============================
Step 3

? (c c465890 c465891)

1. (c c465890 c465892)
2. (p c465892 c465891)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c465891)
|
|1. (~ (c c465890 c465891))
|2. (c c465890 c465892)
|3. (p c465892 c465891)
|
|> hyp
=============================
Step 5

? (c c465890 c465892)

1. (~ (c c465890 c465891))
2. (c c465890 c465892)
3. (p c465892 c465891)

> hyp


LEMMA

If x is disconnected from y and y partially overlaps z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (po y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (dc c471291 c471290)) v (~ (po c471290 c471289))) v (~ (p c471289 c471291)))


> hypdisj
=============================
Step 3

? (~ (p c471289 c471291))

1. (po c471290 c471289)
2. (dc c471291 c471290)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var47 c471289)
|
|1. (p c471289 c471291)
|2. (po c471290 c471289)
|3. (dc c471291 c471290)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p (f465949 Var53 c471289) c471289)
||
||1. (~ (c Var47 c471289))
||2. (p c471289 c471291)
||3. (po c471290 c471289)
||4. (dc c471291 c471290)
||
||> ((p (f465949 X Y) Y) <-- (o X Y))
||=============================
||Step 6
||
||? (o Var53 c471289)
||
||1. (~ (p (f465949 Var53 c471289) c471289))
||2. (~ (c Var47 c471289))
||3. (p c471289 c471291)
||4. (po c471290 c471289)
||5. (dc c471291 c471290)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 7
||
||? (po Var53 c471289)
||
||1. (~ (o Var53 c471289))
||2. (~ (p (f465949 Var53 c471289) c471289))
||3. (~ (c Var47 c471289))
||4. (p c471289 c471291)
||5. (po c471290 c471289)
||6. (dc c471291 c471290)
||
||> hyp
|=============================
|Step 8
|
|? (c (f465949 c471290 c471289) (f465949 c471290 c471289))
|
|1. (~ (c (f465949 c471290 c471289) c471289))
|2. (p c471289 c471291)
|3. (po c471290 c471289)
|4. (dc c471291 c471290)
|
|> ((c X X) <--)
=============================
Step 9

? (~ (c (f465949 c471290 c471289) c471291))

1. (p c471289 c471291)
2. (po c471290 c471289)
3. (dc c471291 c471290)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 10

? (~ (c c471291 (f465949 c471290 c471289)))

1. (c (f465949 c471290 c471289) c471291)
2. (p c471289 c471291)
3. (po c471290 c471289)
4. (dc c471291 c471290)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 11
|
|? (p (f465949 c471290 c471289) c471290)
|
|1. (c c471291 (f465949 c471290 c471289))
|2. (c (f465949 c471290 c471289) c471291)
|3. (p c471289 c471291)
|4. (po c471290 c471289)
|5. (dc c471291 c471290)
|
|> ((p (f465949 X Y) X) <-- (o X Y))
|=============================
|Step 12
|
|? (o c471290 c471289)
|
|1. (~ (p (f465949 c471290 c471289) c471290))
|2. (c c471291 (f465949 c471290 c471289))
|3. (c (f465949 c471290 c471289) c471291)
|4. (p c471289 c471291)
|5. (po c471290 c471289)
|6. (dc c471291 c471290)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 13
|
|? (po c471290 c471289)
|
|1. (~ (o c471290 c471289))
|2. (~ (p (f465949 c471290 c471289) c471290))
|3. (c c471291 (f465949 c471290 c471289))
|4. (c (f465949 c471290 c471289) c471291)
|5. (p c471289 c471291)
|6. (po c471290 c471289)
|7. (dc c471291 c471290)
|
|> hyp
=============================
Step 14

? (~ (c c471291 c471290))

1. (c c471291 (f465949 c471290 c471289))
2. (c (f465949 c471290 c471289) c471291)
3. (p c471289 c471291)
4. (po c471290 c471289)
5. (dc c471291 c471290)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 15

? (dc c471291 c471290)

1. (c c471291 c471290)
2. (c c471291 (f465949 c471290 c471289))
3. (c (f465949 c471290 c471289) c471291)
4. (p c471289 c471291)
5. (po c471290 c471289)
6. (dc c471291 c471290)

> hyp


LEMMA

Case split on whether x is connected to z; if not, then dc x z.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (po y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (dc c476846 c476845)) v (~ (po c476845 c476844))) v ((dc c476846 c476844) v (c c476846 c476844)))


> hypdisj
=============================
Step 3

? (c c476846 c476844)

1. (~ (dc c476846 c476844))
2. (po c476845 c476844)
3. (dc c476846 c476845)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c476846 c476844))

1. (~ (c c476846 c476844))
2. (~ (dc c476846 c476844))
3. (po c476845 c476844)
4. (dc c476846 c476845)

> hyp


LEMMA

If x is connected to z, split on overlap to get ec x z or o x z.
=============================
Step 1

? (all x (all y (all z ((((dc x y) & (po y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (dc c482667 c482666)) v (~ (po c482666 c482665))) v (~ (c c482667 c482665))) v ((ec c482667 c482665) v (o c482667 c482665)))


> hypdisj
=============================
Step 3

? (o c482667 c482665)

1. (~ (ec c482667 c482665))
2. (c c482667 c482665)
3. (po c482666 c482665)
4. (dc c482667 c482666)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c482667 c482665)
|
|1. (~ (o c482667 c482665))
|2. (~ (ec c482667 c482665))
|3. (c c482667 c482665)
|4. (po c482666 c482665)
|5. (dc c482667 c482666)
|
|> hyp
=============================
Step 5

? (~ (ec c482667 c482665))

1. (~ (o c482667 c482665))
2. (~ (ec c482667 c482665))
3. (c c482667 c482665)
4. (po c482666 c482665)
5. (dc c482667 c482666)

> hyp


LEMMA

If x overlaps z and z is not part of x, then either po x z or pp x z.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (po y z)) & (c x z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? (((((~ (dc c488904 c488903)) v (~ (po c488903 c488902))) v (~ (c c488904 c488902))) v (~ (o c488904 c488902))) v ((po c488904 c488902) v (pp c488904 c488902)))


> hypdisj
=============================
Step 3

? (pp c488904 c488902)

1. (~ (po c488904 c488902))
2. (o c488904 c488902)
3. (c c488904 c488902)
4. (po c488903 c488902)
5. (dc c488904 c488903)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c488904 c488902)
|
|1. (~ (pp c488904 c488902))
|2. (~ (po c488904 c488902))
|3. (o c488904 c488902)
|4. (c c488904 c488902)
|5. (po c488903 c488902)
|6. (dc c488904 c488903)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c488902 c488904)
||
||1. (~ (p c488904 c488902))
||2. (~ (pp c488904 c488902))
||3. (~ (po c488904 c488902))
||4. (o c488904 c488902)
||5. (c c488904 c488902)
||6. (po c488903 c488902)
||7. (dc c488904 c488903)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c488904 c488902)
||||
||||1. (~ (p c488902 c488904))
||||2. (~ (p c488904 c488902))
||||3. (~ (pp c488904 c488902))
||||4. (~ (po c488904 c488902))
||||5. (o c488904 c488902)
||||6. (c c488904 c488902)
||||7. (po c488903 c488902)
||||8. (dc c488904 c488903)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c488904 c488902))
|||
|||1. (~ (p c488902 c488904))
|||2. (~ (p c488904 c488902))
|||3. (~ (pp c488904 c488902))
|||4. (~ (po c488904 c488902))
|||5. (o c488904 c488902)
|||6. (c c488904 c488902)
|||7. (po c488903 c488902)
|||8. (dc c488904 c488903)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c488904 c488902))
||
||1. (~ (p c488902 c488904))
||2. (~ (p c488904 c488902))
||3. (~ (pp c488904 c488902))
||4. (~ (po c488904 c488902))
||5. (o c488904 c488902)
||6. (c c488904 c488902)
||7. (po c488903 c488902)
||8. (dc c488904 c488903)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c488902 c488904))
|
|1. (~ (p c488904 c488902))
|2. (~ (pp c488904 c488902))
|3. (~ (po c488904 c488902))
|4. (o c488904 c488902)
|5. (c c488904 c488902)
|6. (po c488903 c488902)
|7. (dc c488904 c488903)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 10
|
|? (~ (p c488902 c488904))
|
|1. (pp c488902 c488904)
|2. (~ (p c488904 c488902))
|3. (~ (pp c488904 c488902))
|4. (~ (po c488904 c488902))
|5. (o c488904 c488902)
|6. (c c488904 c488902)
|7. (po c488903 c488902)
|8. (dc c488904 c488903)
|
|> ((~ (p Z X)) <-- (dc X Y) (po Y Z))
||=============================
||Step 11
||
||? (dc c488904 Var51)
||
||1. (p c488902 c488904)
||2. (pp c488902 c488904)
||3. (~ (p c488904 c488902))
||4. (~ (pp c488904 c488902))
||5. (~ (po c488904 c488902))
||6. (o c488904 c488902)
||7. (c c488904 c488902)
||8. (po c488903 c488902)
||9. (dc c488904 c488903)
||
||> hyp
|=============================
|Step 12
|
|? (po c488903 c488902)
|
|1. (p c488902 c488904)
|2. (pp c488902 c488904)
|3. (~ (p c488904 c488902))
|4. (~ (pp c488904 c488902))
|5. (~ (po c488904 c488902))
|6. (o c488904 c488902)
|7. (c c488904 c488902)
|8. (po c488903 c488902)
|9. (dc c488904 c488903)
|
|> hyp
=============================
Step 13

? (~ (p c488902 c488904))

1. (~ (pp c488904 c488902))
2. (~ (po c488904 c488902))
3. (o c488904 c488902)
4. (c c488904 c488902)
5. (po c488903 c488902)
6. (dc c488904 c488903)

> ((~ (p Z X)) <-- (dc X Y) (po Y Z))
|=============================
|Step 14
|
|? (dc c488904 Var56)
|
|1. (p c488902 c488904)
|2. (~ (pp c488904 c488902))
|3. (~ (po c488904 c488902))
|4. (o c488904 c488902)
|5. (c c488904 c488902)
|6. (po c488903 c488902)
|7. (dc c488904 c488903)
|
|> hyp
=============================
Step 15

? (po c488903 c488902)

1. (p c488902 c488904)
2. (~ (pp c488904 c488902))
3. (~ (po c488904 c488902))
4. (o c488904 c488902)
5. (c c488904 c488902)
6. (po c488903 c488902)
7. (dc c488904 c488903)

> hyp


LEMMA

Proper part decomposes into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c495751 c495750)) v ((tpp c495751 c495750) v (ntpp c495751 c495750)))


> hypdisj
=============================
Step 3

? (ntpp c495751 c495750)

1. (~ (tpp c495751 c495750))
2. (pp c495751 c495750)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f489017 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c495751 c495750)
|
|1. (~ (ntpp c495751 c495750))
|2. (~ (tpp c495751 c495750))
|3. (pp c495751 c495750)
|
|> hyp
=============================
Step 5

? (~ (ec (f489017 c495751 c495750 Var32) c495751))

1. (~ (ntpp c495751 c495750))
2. (~ (tpp c495751 c495750))
3. (pp c495751 c495750)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c495751 Var36)
||
||1. (ec (f489017 c495751 c495750 Var32) c495751)
||2. (~ (ntpp c495751 c495750))
||3. (~ (tpp c495751 c495750))
||4. (pp c495751 c495750)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f489017 c495751 c495750 Var32) c495750)
|
|1. (ec (f489017 c495751 c495750 Var32) c495751)
|2. (~ (ntpp c495751 c495750))
|3. (~ (tpp c495751 c495750))
|4. (pp c495751 c495750)
|
|> ((ec (f489017 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c495751 c495750))
||
||1. (~ (ec (f489017 c495751 c495750 Var32) c495750))
||2. (ec (f489017 c495751 c495750 Var32) c495751)
||3. (~ (ntpp c495751 c495750))
||4. (~ (tpp c495751 c495750))
||5. (pp c495751 c495750)
||
||> hyp
|=============================
|Step 9
|
|? (pp c495751 c495750)
|
|1. (~ (ec (f489017 c495751 c495750 Var32) c495750))
|2. (ec (f489017 c495751 c495750 Var32) c495751)
|3. (~ (ntpp c495751 c495750))
|4. (~ (tpp c495751 c495750))
|5. (pp c495751 c495750)
|
|> hyp
=============================
Step 10

? (~ (tpp c495751 c495750))

1. (ec (f489017 c495751 c495750 Var32) c495751)
2. (~ (ntpp c495751 c495750))
3. (~ (tpp c495751 c495750))
4. (pp c495751 c495750)

> hyp


LEMMA

Refine the overlap case from po or pp to po or tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (po y z)) & (c x z)) & (o x z)) => ((po x z) v ((tpp x z) v (ntpp x z)))))))


> revsk
=============================
Step 2

? (((((~ (dc c502751 c502750)) v (~ (po c502750 c502749))) v (~ (c c502751 c502749))) v (~ (o c502751 c502749))) v ((po c502751 c502749) v ((tpp c502751 c502749) v (ntpp c502751 c502749))))


> hypdisj
=============================
Step 3

? (ntpp c502751 c502749)

1. (~ (tpp c502751 c502749))
2. (~ (po c502751 c502749))
3. (o c502751 c502749)
4. (c c502751 c502749)
5. (po c502750 c502749)
6. (dc c502751 c502750)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c502751 c502749)
|
|1. (~ (ntpp c502751 c502749))
|2. (~ (tpp c502751 c502749))
|3. (~ (po c502751 c502749))
|4. (o c502751 c502749)
|5. (c c502751 c502749)
|6. (po c502750 c502749)
|7. (dc c502751 c502750)
|
|> ((pp Y Z) <-- (dc Y X) (po X Z) (c Y Z) (o Y Z) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (dc c502751 Var32)
|||||
|||||1. (~ (pp c502751 c502749))
|||||2. (~ (ntpp c502751 c502749))
|||||3. (~ (tpp c502751 c502749))
|||||4. (~ (po c502751 c502749))
|||||5. (o c502751 c502749)
|||||6. (c c502751 c502749)
|||||7. (po c502750 c502749)
|||||8. (dc c502751 c502750)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (po c502750 c502749)
||||
||||1. (~ (pp c502751 c502749))
||||2. (~ (ntpp c502751 c502749))
||||3. (~ (tpp c502751 c502749))
||||4. (~ (po c502751 c502749))
||||5. (o c502751 c502749)
||||6. (c c502751 c502749)
||||7. (po c502750 c502749)
||||8. (dc c502751 c502750)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c502751 c502749)
|||
|||1. (~ (pp c502751 c502749))
|||2. (~ (ntpp c502751 c502749))
|||3. (~ (tpp c502751 c502749))
|||4. (~ (po c502751 c502749))
|||5. (o c502751 c502749)
|||6. (c c502751 c502749)
|||7. (po c502750 c502749)
|||8. (dc c502751 c502750)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c502751 c502749)
||
||1. (~ (pp c502751 c502749))
||2. (~ (ntpp c502751 c502749))
||3. (~ (tpp c502751 c502749))
||4. (~ (po c502751 c502749))
||5. (o c502751 c502749)
||6. (c c502751 c502749)
||7. (po c502750 c502749)
||8. (dc c502751 c502750)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c502751 c502749))
|
|1. (~ (pp c502751 c502749))
|2. (~ (ntpp c502751 c502749))
|3. (~ (tpp c502751 c502749))
|4. (~ (po c502751 c502749))
|5. (o c502751 c502749)
|6. (c c502751 c502749)
|7. (po c502750 c502749)
|8. (dc c502751 c502750)
|
|> hyp
=============================
Step 10

? (~ (tpp c502751 c502749))

1. (~ (ntpp c502751 c502749))
2. (~ (tpp c502751 c502749))
3. (~ (po c502751 c502749))
4. (o c502751 c502749)
5. (c c502751 c502749)
6. (po c502750 c502749)
7. (dc c502751 c502750)

> hyp


LEMMA

Combine the local case splits: dc or c; if c then ec or o; if o then po or pp; finally split pp into tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (po y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c510611 c510610)) v (~ (po c510610 c510609))) v (((((dc c510611 c510609) v (ec c510611 c510609)) v (po c510611 c510609)) v (tpp c510611 c510609)) v (ntpp c510611 c510609)))


> hypdisj
=============================
Step 3

? (ntpp c510611 c510609)

1. (~ (tpp c510611 c510609))
2. (~ (po c510611 c510609))
3. (~ (ec c510611 c510609))
4. (~ (dc c510611 c510609))
5. (po c510610 c510609)
6. (dc c510611 c510610)

> ((ntpp Y Z) <-- (dc Y X) (po X Z) (c Y Z) (o Y Z) (~ (po Y Z)) (~ (tpp Y Z)))
|||||=============================
|||||Step 4
|||||
|||||? (dc c510611 Var35)
|||||
|||||1. (~ (ntpp c510611 c510609))
|||||2. (~ (tpp c510611 c510609))
|||||3. (~ (po c510611 c510609))
|||||4. (~ (ec c510611 c510609))
|||||5. (~ (dc c510611 c510609))
|||||6. (po c510610 c510609)
|||||7. (dc c510611 c510610)
|||||
|||||> hyp
||||=============================
||||Step 5
||||
||||? (po c510610 c510609)
||||
||||1. (~ (ntpp c510611 c510609))
||||2. (~ (tpp c510611 c510609))
||||3. (~ (po c510611 c510609))
||||4. (~ (ec c510611 c510609))
||||5. (~ (dc c510611 c510609))
||||6. (po c510610 c510609)
||||7. (dc c510611 c510610)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (c c510611 c510609)
|||
|||1. (~ (ntpp c510611 c510609))
|||2. (~ (tpp c510611 c510609))
|||3. (~ (po c510611 c510609))
|||4. (~ (ec c510611 c510609))
|||5. (~ (dc c510611 c510609))
|||6. (po c510610 c510609)
|||7. (dc c510611 c510610)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 7
|||
|||? (~ (dc c510611 c510609))
|||
|||1. (~ (c c510611 c510609))
|||2. (~ (ntpp c510611 c510609))
|||3. (~ (tpp c510611 c510609))
|||4. (~ (po c510611 c510609))
|||5. (~ (ec c510611 c510609))
|||6. (~ (dc c510611 c510609))
|||7. (po c510610 c510609)
|||8. (dc c510611 c510610)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c510611 c510609)
||
||1. (~ (ntpp c510611 c510609))
||2. (~ (tpp c510611 c510609))
||3. (~ (po c510611 c510609))
||4. (~ (ec c510611 c510609))
||5. (~ (dc c510611 c510609))
||6. (po c510610 c510609)
||7. (dc c510611 c510610)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 9
|||
|||? (c c510611 c510609)
|||
|||1. (~ (o c510611 c510609))
|||2. (~ (ntpp c510611 c510609))
|||3. (~ (tpp c510611 c510609))
|||4. (~ (po c510611 c510609))
|||5. (~ (ec c510611 c510609))
|||6. (~ (dc c510611 c510609))
|||7. (po c510610 c510609)
|||8. (dc c510611 c510610)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 10
|||
|||? (~ (dc c510611 c510609))
|||
|||1. (~ (c c510611 c510609))
|||2. (~ (o c510611 c510609))
|||3. (~ (ntpp c510611 c510609))
|||4. (~ (tpp c510611 c510609))
|||5. (~ (po c510611 c510609))
|||6. (~ (ec c510611 c510609))
|||7. (~ (dc c510611 c510609))
|||8. (po c510610 c510609)
|||9. (dc c510611 c510610)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (ec c510611 c510609))
||
||1. (~ (o c510611 c510609))
||2. (~ (ntpp c510611 c510609))
||3. (~ (tpp c510611 c510609))
||4. (~ (po c510611 c510609))
||5. (~ (ec c510611 c510609))
||6. (~ (dc c510611 c510609))
||7. (po c510610 c510609)
||8. (dc c510611 c510610)
||
||> hyp
|=============================
|Step 12
|
|? (~ (po c510611 c510609))
|
|1. (~ (ntpp c510611 c510609))
|2. (~ (tpp c510611 c510609))
|3. (~ (po c510611 c510609))
|4. (~ (ec c510611 c510609))
|5. (~ (dc c510611 c510609))
|6. (po c510610 c510609)
|7. (dc c510611 c510610)
|
|> hyp
=============================
Step 13

? (~ (tpp c510611 c510609))

1. (~ (ntpp c510611 c510609))
2. (~ (tpp c510611 c510609))
3. (~ (po c510611 c510609))
4. (~ (ec c510611 c510609))
5. (~ (dc c510611 c510609))
6. (po c510610 c510609)
7. (dc c510611 c510610)

> hyp
